COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input macro.tex[let,jmc]
C00005 ENDMK
C⊗;
\input macro.tex[let,jmc]


\ctrline {\undertext {Towards a Logical Reconstruction of Database Theory}}

\yyskip

\ctrline {Raymond Reiter}

\ctrline {Department of Computer Science}

\ctrline {The University of British Columbia}

\yyskip

\ctrline {ABSTRACT}

\yyskip

I shall argue that databases can and should be viewed as special theories
of first order logic, namely theories incorporating the following assumptions:

\display 60pt: 1.: The domain closure assumption:  The individuals occurring
in the database are all and only the existing individuals.

\display 60pt: 2.: The unique name assumption:  Individuals with unique names
are unique. 

\display 60pt: 3.: The closed world assumption:  If a positive fact is not
derivable from the database, then its negation may be inferred.

\noindent Of these, the closed world assumption is by far the most difficult
to formalize.  Recent work in Artificial Intelligence on non monotonic
reasoning, specifically McCarthy's concept of circumscription, seems to
characterize this notion correctly.

I shall further argue that logic provides a correct approach to the treatment
of

\display 60pt: 1.: Queries and their answers.

\display 60pt: 2.: Null values.

\display 60pt: 3.: Integrity constraints.  What are they and how should they
be enforced?

\display 60pt: 4.: Conceptual modelling.  How can the relational model be 
extended to incorporate more real world semantics?

It will follow that a logical foundation for database theory admits correctness
proofs for a variety of central issues, e.g., correctness of query
evaluators for databases with null values, and correctness of integrity
maintenance algorithms.

\vfill \eject

\end